package com.googlecode.kipler.transformations;

import com.googlecode.kipler.syntax.concept.AtConcept;
import com.googlecode.kipler.syntax.concept.BooleanConcept;
import com.googlecode.kipler.syntax.concept.BooleanConstructor;
import com.googlecode.kipler.syntax.concept.Bottom;
import com.googlecode.kipler.syntax.concept.CardinalityRestriction;
import com.googlecode.kipler.syntax.concept.Concept;
import com.googlecode.kipler.syntax.concept.ConceptName;
import com.googlecode.kipler.syntax.concept.ConceptVisitor;
import com.googlecode.kipler.syntax.concept.InequalityConstructor;
import com.googlecode.kipler.syntax.concept.NaryBooleanConcept;
import com.googlecode.kipler.syntax.concept.Nominal;
import com.googlecode.kipler.syntax.concept.QualifiedNoRestriction;
import com.googlecode.kipler.syntax.concept.RoleQuantification;
import com.googlecode.kipler.syntax.concept.Top;

/**
 * 
 * @author İnanç Seylan
 * 
 */
public class ConceptSimplificationVisitor implements ConceptVisitor {
	private Concept normalForm;

	public Concept getNormalForm() {
		return normalForm;
	}

	public void visitBooleanConcept(BooleanConcept bd) {
		normalForm = bd;
		ConceptSimplificationVisitor visitor = new ConceptSimplificationVisitor();
		bd.getLhs().accept(visitor);
		bd.setLhs(visitor.getNormalForm());
		visitor = new ConceptSimplificationVisitor();
		bd.getRhs().accept(visitor);
		bd.setRhs(visitor.getNormalForm());
		if (bd.getLhs().equals(bd.getRhs())) {
			normalForm = bd.getLhs();
		} else if (bd.getConstructor() == BooleanConstructor.UNION) {
			if (bd.getLhs().equals(new Top()) || bd.getRhs().equals(new Top())) {
				normalForm = new Top();
			} else if (bd.getLhs().equals(new Bottom())) {
				normalForm = bd.getRhs();
			} else if (bd.getRhs().equals(new Bottom())) {
				normalForm = bd.getLhs();
			}
		} else if (bd.getConstructor() == BooleanConstructor.INTERSECTION) {
			if (bd.getLhs().equals(new Bottom())
					|| bd.getRhs().equals(new Bottom())) {
				normalForm = new Bottom();
			} else if (bd.getLhs().equals(new Top())) {
				normalForm = bd.getRhs();
			} else if (bd.getRhs().equals(new Top())) {
				normalForm = bd.getLhs();
			}
		}
	}

	public void visitConceptName(ConceptName c) {
		// nothing to do
		normalForm = c;
	}

	public void visitRoleQuantification(RoleQuantification restriction) {
		normalForm = restriction;
		ConceptSimplificationVisitor visitor = new ConceptSimplificationVisitor();
		restriction.getConcept().accept(visitor);
		restriction.setConcept(visitor.getNormalForm());
	}

	public void visitQualifiedNoRestriction(QualifiedNoRestriction restriction) {
		if (restriction.getNo() < 0) {
			normalForm = new Bottom();
		} else if (restriction.getNo() == 0
				&& restriction.getConstructor() == InequalityConstructor.AT_LEAST) {
			// >=(0, R, C) <-> T
			normalForm = new Top();
		} else if (restriction.getNo() == 0
				&& restriction.getConstructor() == InequalityConstructor.AT_MOST) {
			// <=(0, R, C) <-> all(R, ~C)
			ConceptSimplificationVisitor visitor = new ConceptSimplificationVisitor();
			restriction.getConcept().copy().toggleNegated().accept(visitor);
			normalForm = new RoleQuantification(
					RoleQuantification.Constructor.ALL, restriction.getRole(),
					visitor.getNormalForm());
		} else if (restriction.getNo() == 1
				&& restriction.getConstructor() == InequalityConstructor.AT_LEAST) {
			// >=(1, R, C) <-> some(R, C)
			ConceptSimplificationVisitor visitor = new ConceptSimplificationVisitor();
			restriction.getConcept().accept(visitor);
			normalForm = new RoleQuantification(
					RoleQuantification.Constructor.SOME, restriction.getRole(),
					visitor.getNormalForm());
		} else {
			ConceptSimplificationVisitor visitor = new ConceptSimplificationVisitor();
			restriction.getConcept().accept(visitor);
			restriction.setConcept(visitor.getNormalForm());
			normalForm = restriction;
		}
	}

	public void visitNominal(Nominal nominal) {
		// nothing to do
		normalForm = nominal;
	}

	@Override
	public void visitAtConcept(AtConcept c) {
		normalForm = c;
		if (c.getConcept() instanceof Nominal) {
			Nominal nom = (Nominal) c.getConcept();
			if (c.getName().equals(nom.getName()) && nom.isNegated()) {
				normalForm = new Bottom();
			} else if (c.getName().equals(nom.getName()) && !nom.isNegated()) {
				normalForm = new Top();
			}
		} else if (c.getConcept() instanceof Top) {
			normalForm = new Top();
		} else if (c.getConcept() instanceof Bottom) {
			normalForm = new Bottom();
		}
	}

	@Override
	public void visitBottom(Bottom bottom) {
		normalForm = bottom;
	}

	@Override
	public void visitCardinalityRestriction(CardinalityRestriction restriction) {
		// TODO Auto-generated method stub

	}

	@Override
	public void visitTop(Top top) {
		normalForm = top;
	}

	@Override
	public void visitNaryBooleanConcept(NaryBooleanConcept c) {
		NaryBooleanConcept simplified = new NaryBooleanConcept(c
				.getConstructor());
		for (Concept i : c.getOperands()) {
			ConceptSimplificationVisitor visitor = new ConceptSimplificationVisitor();
			i.accept(visitor);
			simplified.addOperand(visitor.getNormalForm());
		}
		normalForm = simplified;
		if (simplified.getConstructor() == BooleanConstructor.UNION) {
			if (simplified.getOperands().contains(new Top())) {
				normalForm = new Top();
			} else if (simplified.getOperands().contains(new Bottom())) {
				simplified.getOperands().remove(new Bottom());
			}
		} else if (simplified.getConstructor() == BooleanConstructor.INTERSECTION) {
			if (simplified.getOperands().contains(new Bottom())) {
				normalForm = new Bottom();
			} else if (simplified.getOperands().contains(new Top())) {
				simplified.getOperands().remove(new Top());
			}
		}
	}

}
